$f$'${\it Ia}$ $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\lambda$$a$.inl ($f$($a$))  o ${\it Ia}$